predicate are_mirrored(xs: array<int>, ys: array<int>)
reads xs, ys
{
	xs.Length == ys.Length && forall k :: 0 <= k < xs.Length ==> xs[k] == ys[ys.Length - 1 - k]
}

method reverse_array(xs: array<int>) returns (ys: array<int>)
ensures xs.Length == ys.Length
{
	ys := new int[xs.Length];
	// using the forall statement, dafny can automatically infer an invariant of the sort
	// forall k :: 0 <= k < i ==> ys[ys.Length - 1 - k] == xs[k]
	// where i is an internally used loop variable
	forall k | 0 <= k < xs.Length
	{
		ys[ys.Length - 1 - k] := xs[k];
	}
	// essentially, after the forall statement, dafny can be sure that
	// assert forall k :: 0 <= k < xs.Length ==> ys[ys.Length - 1 - k] == xs[k]
	return ys;
}

predicate all_even(xs: array<int>)
reads xs
{
	forall k :: 0 <= k < xs.Length ==> xs[k] % 2 == 0
}

method double_all(xs: array<int>)
modifies xs
ensures all_even(xs)
{
	var i := 0;
	// in this loop, dafny can not automatically infer the necessary invariant,
	// which is a quantified expression involving all values that have already been evaluated
	while i < xs.Length
	invariant 0 <= i <= xs.Length
	invariant forall k :: 0 <= k < i ==> xs[k] % 2 == 0
	{
		xs[i] := xs[i] * 2;
		i := i + 1;
	}
}